$\forall$$A$:Type, $F$:($A$$\rightarrow$prop\{i:l\}), $L$:($A$ List).
\\[0ex]($\forall$$k$:$A$. decidable($F$($k$))) $\Rightarrow$ decidable(l\_exists($L$; $A$; $k$.$F$($k$)))